The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
member(x, cons(y, ys)) →⁺ if(eq(x, y), true, member(x, ys))
gives rise to a decreasing loop by considering the right hand sides subterm at position [2].
The pumping substitution is [ys / cons(y, ys)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
member, eq, choice, guess, verify

They will be analysed ascendingly in the following order:
eq < member
member < verify
choice < guess

(8) Obligation:

TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
eq, member, choice, guess, verify

They will be analysed ascendingly in the following order:
eq < member
member < verify
choice < guess

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol eq.

(10) Obligation:

TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
member, choice, guess, verify

They will be analysed ascendingly in the following order:
member < verify
choice < guess

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol member.

(12) Obligation:

TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
choice, guess, verify

They will be analysed ascendingly in the following order:
choice < guess

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol choice.

(14) Obligation:

TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
guess, verify

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol guess.

(16) Obligation:

TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
verify

(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol verify.

(18) Obligation:

TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.